Nuprl Lemma : node_wf
4,23
postcript
pdf
E
:Type,
x
,
y
:Tree(
E
). tree_node(<
x
,
y
>)
Tree(
E
)
latex
Definitions
tree_node(<
x
,
y
>)
,
tree_node(
x
)
,
Tree(
E
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
tree
wf
,
tree
node
wf2
origin
E:Type, x, y:Tree(E). tree_node(<x, y>) 
Tree(E) E:Type, x, y:Tree(E). tree_node(<x, y>) Tree(E) x:A. B(x) T